
module Transition =
struct
  type t = Tau | Action of string
  let compare = Pervasives.compare
  let string_of =
  function
      Tau -> "-"
    | Action s -> s
end

module TransitionSet = Set.Make(Transition)

module Make =
  functor (State : Set.OrderedType) ->
    struct
      type state_t =
	  { state : State.t;
	    index : int;
	    mutable next : (Transition.t * state_t) list;
	  }

      module HashedState =
      struct
	type t = State.t
	let equal x y = State.compare x y = 0
	let hash = Hashtbl.hash
      end

      module StateMap = Hashtbl.Make(HashedState)

      module StateSet = Set.Make(State)

      type t =
	  { mutable next_index : int;
	    mutable state_map : state_t StateMap.t;
	  }

      let make () =
	{ next_index = 0;
	  state_map = StateMap.create 1023;
	}

      let mk_state v index =
	{ state = v;
	  index = index;
	  next = [];
	}

      let get_states a =
	let pl = ref [] in
	  StateMap.iter
	    (fun p _ -> pl := p :: !pl)
	    a.state_map;
	  !pl

      let size a = List.length (get_states a)

      let get_internal_state a = StateMap.find a.state_map
      let get_external_state s = s.state

      let get_state a p =
	try
	  (false, get_internal_state a p)
	with
	    Not_found ->
	      let s = mk_state p a.next_index in
		a.next_index <- a.next_index + 1;
		StateMap.add a.state_map p s;
		(true, s)

      let make_state a p = fst (get_state a p)

      let get_state_index a p = (get_internal_state a p).index

      let get_state_transitions a p =
	let s = get_internal_state a p in
	  List.map
	    (fun (t, s') -> t, get_external_state s')
	    s.next

      let add_transition a p t p' =
	let s = get_internal_state a p
	and s' = get_internal_state a p' in
	  s.next <- (t, s') :: s.next

      let to_graph default_node_shape string_of_state string_of_transition ch a name =
	Printf.fprintf ch "digraph \"%s\" {\n" name;
	Printf.fprintf ch "  d2tdocpreamble = \"\\usetikzlibrary{automata}\";\n";
	Printf.fprintf ch "  d2tfigpreamble = \"\\tikzstyle{every state}=[draw=blue!50,very thick,fill=blue!20]\"\n";
(* 	Printf.fprintf ch "  node [shape=%s,fixedsize=true,width=0.3,height=0.3];\n" default_node_shape; *)
	Printf.fprintf ch "  node [style=state];\n";
	Printf.fprintf ch "  edge [lblstyle=auto];\n";
	Printf.fprintf ch "  q0 [style=state,initial];\n";
	StateMap.iter
	  (fun _ s ->
	     Printf.fprintf ch "  q%d [label=\"q%d\",texlbl=\"$%s$\"];\n"
	       s.index s.index
	       (string_of_state (get_external_state s))
	  )
	  a.state_map;
	StateMap.iter
	  (fun _ s ->
	     List.iter
	       (fun (t, s') ->
		  Printf.fprintf ch "  q%d -> q%d [label=\"%s\",texlbl=\"$%s$\"];\n"
		    s.index s'.index
		    (Transition.string_of t)
		    (string_of_transition t)
	       )
	       s.next
	  )
	  a.state_map;
	Printf.fprintf ch "}\n"

      let pp string_of_state string_of_transition a =
	StateMap.iter
	  (fun p s ->
	    List.iter
	      (fun (t, s') ->
		Printf.printf "%s --%s--> %s\n" (string_of_state p) (string_of_transition t) (string_of_state (get_external_state s'))
	      )
	      s.next
	  )
	  a.state_map

      let reachable a t s =
	let s' = get_internal_state a s in
	  List.fold_right
	    (fun (_, s'') -> StateSet.add (get_external_state s''))
	    (List.filter (fun (t', _) -> t = t') s'.next)
	    StateSet.empty

      let reachable_set a t sset =
	StateSet.fold (fun s -> StateSet.union (reachable a t s)) sset StateSet.empty

      let tau_closure_set a =
	FunAux.limit StateSet.equal (fun pset -> StateSet.union pset (reachable_set a Transition.Tau pset))

      let tau_closure a p = tau_closure_set a (StateSet.singleton p)

	(*Funtore ReadySet*)
      module OrderedAction = 
	struct
 	 type t = string
  	 let compare = Pervasives.compare
	 let string_of s = s
      end

	(*Modulo che utilizzo per la costruzione di ActionSet contenenti azioni*)
      module ReadySet = Set.Make(OrderedAction)

      let succ a p =
	let s = get_internal_state a p in
	  List.fold_right
	    (fun (t, _) -> TransitionSet.add t)
	    s.next
	    TransitionSet.empty

      let succ_set a pset =
	StateSet.fold (fun p -> TransitionSet.union (succ a p)) pset TransitionSet.empty

      let ready_set a s = 
	let s' = get_internal_state a s in
	  List.fold_right
	    (function
		 (Transition.Action a, _) -> ReadySet.add a
	       | (Transition.Tau, _) -> fun x -> x)
	    (s'.next)
	    ReadySet.empty	

      let ready_set_set a sset =
  	StateSet.fold (fun s -> ReadySet.union (ready_set a s)) sset ReadySet.empty

      (*Funtore AcceptanceSet*)
      module OrderedReadySet = 
      struct
        type t = ReadySet.t
        let compare = ReadySet.compare
      end

      (*Modulo che utilizzo per la costruzione di AcceptanceSet contenenti ReadySet*)
      module AcceptanceSet = Set.Make(OrderedReadySet)

      let is_stable a p =
	StateSet.is_empty (reachable a Transition.Tau p)

      (*Funzione che dato in ingresso un automa e uno stato mi calcola l'AcceptanceSet dello stato in questo modo:
	- calcola la tau-closure dello stato in input;
	- calcola l'acceptance-set come unione dei ready-set degli stati tau-closed da quello di input*)
      let acceptance_set a p =
        StateSet.fold
          (fun q -> AcceptanceSet.add (ready_set a q))
          (StateSet.filter (is_stable a) (tau_closure a p))
          AcceptanceSet.empty

      let acceptance_set_set a sset = 
       StateSet.fold (fun s -> AcceptanceSet.union (acceptance_set a s)) sset AcceptanceSet.empty

     (*Funzione che dato in ingresso un automa e uno stato ti calcola l'AcceptanceSet minimo dello stato in input*)
      let min_acceptance_set aset =
	AcceptanceSet.filter
          (fun rset -> 
	     AcceptanceSet.for_all
	       (fun rset' -> 
		  not (ReadySet.subset rset' rset) || ReadySet.equal rset' rset) aset)
          aset

     (*Funzione che dato un AcceptanceSet calcola l'unione dei ReadySet*)
      let union_acceptance_set aset = 
	AcceptanceSet.fold ReadySet.union aset ReadySet.empty  

     (*Funzione che dato in ingresso un automa e uno stato calcola l'AcceptanceSet caratteristico dello stato in input*)
      let car_acceptance_set aset = 
	let min_aset = min_acceptance_set aset in
	let uset = union_acceptance_set aset in
          if ReadySet.equal uset (union_acceptance_set min_aset) then
            min_aset
          else 
            AcceptanceSet.add uset min_aset 

      let sat_acceptance_set aset =
	let uset = union_acceptance_set aset in
	let rec subsets s =
	  if ReadySet.is_empty s then
	    AcceptanceSet.singleton ReadySet.empty
	  else
	    let a = ReadySet.choose s in
	    let sset = subsets (ReadySet.remove a s) in
	    let sset' =
	      AcceptanceSet.fold
		(fun rset -> AcceptanceSet.add (ReadySet.add a rset))
		sset
		AcceptanceSet.empty
	    in
	      AcceptanceSet.union sset sset'
	in
	  AcceptanceSet.filter
	    (fun rset ->
	       AcceptanceSet.exists
		 (fun rset' -> ReadySet.subset rset' rset)
		 aset)
	    (subsets uset)
    end
